Session Types
Session types plan the communication sequence for concurrent programs by the direction and datatype of messages. Checking programs for compliance with these plans ensures that communication errors and deadlocks do not occur.
Seminar
In the seminar, we will explore session types using the RUMPSTEAK framework written in Rust. Introduce the concept of (multiparty) session types using example code from RUMPSTEAK. Your paper should answer the following questions:
- What are (multiparty) session types?
- How does asynchronous execution differ from synchronous execution?
- What are the challenges of reordering messages?
- How does RUMPSTEAK achieve safe message reordering?
- Are there other session type implementations with similar asynchrony features?
Project
In the project, we will develop a library for programming with session types in Lean. There are some existing implementations in Rust and Haskell that can be used as a reference.
We will start with the implementation of binary session types, for interaction between two programs, and then look into for further features such as multi-party session types, for example.